A:Type, I:MaInterface(A), i:Id.
(i  ma-interface-locs(I))
 (k:Knd.
 (k  ma-interface-dom(I;i))
  (ma-interface-code(I;i;k)
  ( State(ma-interface-ds(I;i))ma-interface-valtype(I;i;k)(A + Top))) 

latex

Definitions	x:A. B(x), ma-interface-ds(I;i), State(ds), ma-interface-valtype(I;i;k), Top, left + right, x:AB(x), Type, ma-interface-info(I;i;k), t.1, t  T, t.2, ma-interface-code(I;i;k), Knd, (x  l), P  Q, Id, MaInterface(T)
Lemmas	subtype rel self